es:ES{i}, A:Type{i}, l:IdLnk, tg:Id, ds:x:Id fp Type{i},
conds:k:Knd fp V:Type{i}  (State(ds)V(A + Top)).
triggers-glued-p(es; A; l; tg; ds; conds)  {i'} 

latex

Definitions	t  T, , {T}, SQType(T), P  Q, x:A. B(x)
Lemmas	lsrc wf, es-triggers-params-consistent wf, Id sq